n:. n  rationals 

latex

Definitions	top, qeq(r; s), if b then t else f fi , tt, b-union(A; B), rationals, t  T, x:A. B(x), P  Q, P  Q, P  Q, P  Q
Lemmas	assert of eq int, eq int wf, eqtt to assert, isint-int, int nzero wf, ifthenelse wf, btrue wf, rationals wf